the_w:World, i:Id, a:Action(i). isnull(a)  valtype(i;a)  Type 

latex

Definitions	World, Action(i), isnull(a), valtype(i;a), kind(a), w.TA, w.M, kindcase(k; a.f(a); l,t.g(l;t) ), x,y. t(x;y), IdLnk, isl(x), , Id, Action(dec), b, outr(x), A, P  Q, False, True, 1of(t), x. t(x), x:A. B(x), Knd, w-action-dec(TA;M;i), true, t  T, false
Lemmas	bfalse wf, btrue wf, Knd wf, pi1 wf, Id wf, w-action-dec wf, action wf, assert wf, not wf, IdLnk wf, kindcase wf, world wf